/**
 * 
 */
package tests;

import static org.junit.Assert.*;

import operateurs.Et;
import operateurs.Implique;
import operateurs.Non;
import operateurs.Ou;

import org.junit.Before;
import org.junit.Test;

import quantifieurs.Existe;
import quantifieurs.PourTout;
import termes.Variable;

import base.Atome;
import base.Formule;

/**
 * @author roulleau
 *
 */
public class FormuleTest {

	// formules originelles
	private Formule t0, t1, t2, t3;
	
	/**
	 * initialisation des formules originelles
	 * @throws java.lang.Exception
	 */
	@Before
	public void setUp() throws Exception {
		//formule de base(temoin)
		this.t0 = new Non(new Atome("A"));
		
		//formule d'exemple principal
		this.t1 = new Et(new PourTout(new Variable("x"), new Implique(new Atome("bebe", new Variable("x")), new Atome("illogique", new Variable("x")))),
				new Et( new PourTout(new Variable("x"), new Implique(new Atome("crocodile", new Variable("x")), new Non(new Atome("meprise", new Variable("x"))))),
						new PourTout(new Variable("x"), new Implique(new Atome("illogique", new Variable("x")), new Atome("meprise", new Variable("x"))))
						));
		
		//formule de test de la negation
		this.t2 = new Existe(new Variable("x"), new PourTout(new Variable("y"),
					new Et(new Atome("dragon", new Variable("x")), new Atome("vert",new Variable("y")) )));
	
		//formule de test du transport de la negation
		this.t3 = new Existe(new Variable("t"), new Non(new Non(new Non(new Ou(new Atome("A"), new Non(new Et(new Atome("B"), new Atome("C"))))))));
	
	}
	
	/**
	 * Test method for {@link base.Formule#isSame(base.Formule)}
	 */
	@Test
	public void testIsSame(){
		org.junit.Assert.assertTrue(t0.isSame(t0));

		org.junit.Assert.assertTrue(new Non(t1).isSame(new Non(t1)));
		org.junit.Assert.assertFalse(t0.isSame(t1));
	}
	
	/**
	 * Test method for {@link base.Formule#supprimeConnecteurs()}.
	 */
	@Test
	public void testSupprimeConnecteurs() {
		Formule r0 = new Non(new Atome("A"));
		Formule r1= new Et(new PourTout(new Variable("x"), new Ou(new Non(new Atome("bebe", new Variable("x"))), new Atome("illogique", new Variable("x")))),
				new Et( new PourTout(new Variable("x"), new Ou(new Non(new Atome("crocodile", new Variable("x"))), new Non(new Atome("meprise", new Variable("x"))))),
						new PourTout(new Variable("x"), new Ou(new Non(new Atome("illogique", new Variable("x"))), new Atome("meprise", new Variable("x"))))
						));
				/*new Ou(
				new Existe(new Variable("x"), new Et(
						new Atome("bebe", new Variable("x")), new Non(new Atome("illogique", new Variable("x"))) ),
				new	Ou(new Existe(new Variable("x"), new Et()))	)))
		*/
		Formule r2 = t2;
		Formule r3 = t3;
		
		org.junit.Assert.assertTrue(r0.isSame(t0.supprimeConnecteurs()));
		org.junit.Assert.assertTrue(r1.isSame(t1.supprimeConnecteurs()));
		org.junit.Assert.assertTrue(r2.isSame(t2.supprimeConnecteurs()));
		org.junit.Assert.assertTrue(r3.isSame(t3.supprimeConnecteurs()));
	}

	/**
	 * Test method for {@link base.Formule#negation()}.
	 */
	@Test
	public void testNegation() {
		
		//Formule r1 = new Ou(new Existe(new Variable(x), new Implique))
		org.junit.Assert.assertTrue(new Atome("A").isSame(t0.negation()));
		
	}

	/**
	 * Test method for {@link base.Formule#descendreNegation(boolean)}.
	 */
	@Test
	public void testDescendreNegation() {
		fail("Not yet implemented"); // TODO
	}

}
